\documentclass{article}
\usepackage{amsmath}
\begin{document}

\title{A Proof of Correctness of the BTO Linear Algebra Compiler}
\date{\today}
\author{Jonathan Turner \and Thomas Nelson}

\maketitle

Compilers are complicated pieces of software, often without
accompanying proofs of their correctness.  One exception is the
\textit{compcert} project of Leroy et al., which proved a C compiler
correct.  

In our project, we prove the correctness of a simple linear
algebra compiler.  The translation of mathematical descriptions of matrix
operations to data structures and algorithms which can be run on a
computer is a non-trivial task.  

Our input for this compiler is a AST of linear algebra
expressions.  The linear algebra subset we implemented in Isabelle is
matrix scaling, addition, and multiplication of two-dimentional
matrices.  From this input AST we generate two things:
the mathematical description of the expression and the BTO computation
over data structures.

To represent the mathematical description, which form the basis
for our proof of correctness, we chose to describe the mathematical
functions in Isabelle using shallow embedding.  The mathematical definition treats matrices as functions of type

\begin{verbatim}(nat x nat) => nat
\end{verbatim}  

Each operation returns a new anonymous
function which representing the result matrix.  For example, if A is an \(m\) x \(p\) matrix and B
is a \(p\) x \(n\) matrix, then 

\begin{equation}
C(i, j) = \sum_{k=0}^{p-1} A(i, k) * B(k, j) \qquad 0 \le i < m, 0 \le j < n
\end{equation}


The BTO compiler converts the expression provided into a series of
calls to Isabelle functions which take linked lists which represent
our matrices and output linked lists which represent the results.  Our proof shows the equivalence of the BTO compiler's output
with the mathematical evaluation of the expression for valid indices.
The main theorem is

\begin{verbatim}
[| wf_expression expression m n |] ==> 
  matrix_equivalence (math_eval expression) (compute expression) m n
\end{verbatim}

Even for this limited language, the proof of correctness for all three
operations was complicated.  The most difficult of which was matrix
multiplication, where the order of operations expressed in the
mathematical description differs from the order expressed in the BTO
representation.  Possible future work could include adding new
operations or a more realistic target language.

\end{document}
